package controller.solver;

import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.Scanner;
import java.util.concurrent.Semaphore;

import model.solver.ESolver;
import model.solver.RSatParameter;
import model.solver.SolverParameter;
import model.solver.SolverResult;
import model.solver.SolverResultStatus;

/**
 * This class is a implementation of Solver for RSat.
 * 
 * @author GRONOWSKI Stephane svan001@aol.com
 * 
 *         igsat 2010
 * 
 */
public class RSat extends Solver {

	public static final String	EXEC					= "rsat";
	public static final String	DESCRIPTION				= "Result of the minisat execution";

	public static final String	UNKNOW_TOKEN			= "UNKNOW";
	public static final String	DECISION_TOKEN			= "Decisions: ";
	public static final String	CONFLICT_TOKEN			= "Conflicts: ";
	public static final String	BEGIN_PRINT_TOKEN		= "\nv";
	public static final String	END_PRINT_TOKEN			= "\nc";

	// public static final int DEFAULT_RETURN_VALUE = 0;

	/** The default value that is associate to a UNSATISFIABLE result */
	public static final int		RETURN_UNSATISFIABLE	= 20;
	/** The default value that is associate to a SATISFIABLE result */
	public static final int		RETURN_SATISFIABLE		= 10;

	public static final int		DEFAULT_NB_PARAM		= 2;
	public static final int		NB_PARAM_TIMEOUT		= 2;
	public static final int		NB_PARAM_PRINT_SOLUTION	= 1;

	private RSatParameter		param;

	/**
	 * Create a RSat solver.
	 * 
	 * @param directory
	 *            directory where the executable file is.
	 * @throws IOException
	 *             if there is a problem with the file.
	 */
	public RSat(File directory) throws IOException {
		if (!directory.isDirectory() || !new File(directory, EXEC).isFile())
			throw new IllegalArgumentException();

		type = ESolver.RSAT;
		param = new RSatParameter();
		try
		{
			path = directory.getCanonicalPath() + File.separator + EXEC;
		} catch (IOException e)
		{
			e.printStackTrace();
			throw new IOException();
		}
	}

	@Override
	public boolean checkParameter() {
		return param.basicCheck();
	}

	@Override
	public SolverParameter getSolverParameter() {
		return param;
	}

	/**
	 * 
	 * @return the {@link RSatParameter}
	 */
	public RSatParameter getRSatParameter() {
		return param;
	}

	@Override
	public String[] getCommandLine(String cnfFile) {
		// TODO ajouter les autre arg
		String[] tab;
		int nbParam = DEFAULT_NB_PARAM;

		if (param.needTimeOut())
			nbParam += NB_PARAM_TIMEOUT;
		if (param.isPrintSolution())
			nbParam += NB_PARAM_PRINT_SOLUTION;

		tab = new String[nbParam];

		int nb = 0;
		// bash
		tab[nb++] = path;
		// stdin
		tab[nb++] = cnfFile;// correctFormatForLinux(cnfFile);
		if (param.needTimeOut())
		{// gere timeout
			tab[nb++] = "-t";
			tab[nb++] = String.valueOf(param.getTimeOut() / 1000);
		}
		if (param.isPrintSolution())
			{
			tab[nb++] = "-s";
			System.out.println("set print slolution");
			}

		return tab;
	}

	@Override
	public boolean hasTimeout() {
		return true;
	}

	@Override
	public SolverResult runSolver(String[] cmd, Semaphore manager) {
		// TODO copier coller
		SolverResult res = new SolverResult();

		BufferedReader input = null;
		BufferedReader inerr = null;
		try
		{// lance le processus
			res.setBegin(System.currentTimeMillis());
			setRunning(true);

			try
			{
				process = Runtime.getRuntime().exec(cmd);
			} catch (IOException e)
			{
				throw e;
			}
			finally
			{// libere les sem
				sem.release();
				if (manager != null)
					manager.release();
			}

			String line;
			input = new BufferedReader(new InputStreamReader(process.getInputStream()));
			inerr = new BufferedReader(new InputStreamReader(process.getErrorStream()));

			while ((line = input.readLine()) != null)
			{ // verifie les stdin
				System.out.println(line);
				res.addStdin(line + "\n");
			}
			while ((line = inerr.readLine()) != null)
			{ // verifie les stderr
				System.out.println(line);
				res.addStderr(line + "\n");
			}
		} catch (IOException e)
		{
			// e.printStackTrace();
			res.setStatus(SolverResultStatus.PROBLEM);
			if (process != null)
				process.destroy();
		}
		finally
		{
			try
			{
				if (input != null)
					input.close();
				if (inerr != null)
					inerr.close();
				if (process != null)
					res.setExitVal(process.waitFor());
			} catch (Exception e)
			{
				e.printStackTrace();
				res.setStatus(SolverResultStatus.PROBLEM);
			}
			finally
			{
				try
				{
					sem.acquire();
				} catch (InterruptedException e)
				{
					// TODO Auto-generated catch block
					e.printStackTrace();
					return null;
				}
				setRunning(false);
			}

		}
		// terminer
		res.setEnd(System.currentTimeMillis());

		// System.out.println("val de retour " + res.getExitVal());

		// s'occupe du status
		if (hasBeenStop())
			res.setStatus(SolverResultStatus.STOP);
		if (res.getStdin().indexOf(UNKNOW_TOKEN) != -1)
			res.setStatus(SolverResultStatus.TIMEOUT_REACHED);
		else
			if (res.getStatus() == SolverResultStatus.PROBLEM)
				switch (res.getExitVal()) {
				case RETURN_UNSATISFIABLE:
					res.setStatus(SolverResultStatus.UNSATISFIABLE);
					setLastResult(res);
					break;
				case RETURN_SATISFIABLE:
					res.setStatus(SolverResultStatus.SATISFIABLE);
					setLastResult(res);
					break;

				default:
					res.setStatus(SolverResultStatus.PROBLEM);
				}

		// dernier details
		res.setDescription(DESCRIPTION);

		sem.release();
		return res;
	}

	/*
	 * Obtain more information about the result using stderr/stdin.
	 */
	private void setLastResult(SolverResult res) {
		int index = res.getStdin().indexOf(BEGIN_PRINT_TOKEN);
		if (index != -1)
		{// recupere l solution
			String tmp = res.getStdin().substring(index + BEGIN_PRINT_TOKEN.length());
			int indexFin = tmp.indexOf(END_PRINT_TOKEN);

			res.setSolution(tmp.substring(0, indexFin));
		}

		// recupere details
		index = res.getStdin().indexOf(DECISION_TOKEN);
		Scanner scan = new Scanner(res.getStdin().substring(index + DECISION_TOKEN.length()));

		// recupere le nb de decision
		res.setDecisions(scan.nextInt());

		// recupere le nb de conflict
		index = res.getStdin().indexOf(CONFLICT_TOKEN);
		scan = new Scanner(res.getStdin().substring(index + CONFLICT_TOKEN.length()));
		res.setConflics(scan.nextInt());
	}

}
